Opaque predicates are often used for code obfuscation as they are complicating code analysis, especially when it's done statically. An example of an opaque predicate in x86 assembly is a conditional jump which is always continuing execution either at taken or not taken branch - regardless of user input, OS version, etc. The other, never taken branch, usually contains complete junk code or code belonging to some other routine. If we can prove that a conditional jump can be eliminated (either replaced with unconditional jump or completely removed/replaced with NOPs), then we can significantly improve and simplify code analysis.
I've decided to start playing with Z3, a powerful SMT solver developed by Microsoft which, amongst many other things, can also be used for proving the existance of opaque predicates in code.